Nuprl Lemma : es-loc-pred-plus
0,22
postcript
pdf
es
:ES,
x
,
y
:E. (
x
x
,
y
.
first(
y
) &
x
= pred(
y
)^+
y
)
loc(
x
) = loc(
y
)
Id
latex
Definitions
x
f
y
,
R
^+
,
ES
,
t
T
,
x
:
A
B
(
x
)
,
x
:
A
B
(
x
)
,
loc(
e
)
,
Id
,
s
=
t
,
es-pred?(
es
)
,
pred(
e
)
,
E
,
first(
e
)
,
b
,
A
,
A
&
B
,
x
.
A
(
x
)
,
rel_exp(
T
;
R
;
n
)
,
f
(
a
)
,
P
Q
,
x
:
A
.
B
(
x
)
,
,
#$n
,
n
-
m
,
a
<
b
,
Void
,
False
,
A
B
,
{
x
:
A
|
B
(
x
) }
,
,
,
Type
,
Prop
,
P
&
Q
,
x
:
A
.
B
(
x
)
,
b
,
,
i
=
j
,
P
Q
,
Unit
,
left
+
right
,
{
T
}
,
SQType(
T
)
,
s
~
t
,
P
Q
,
Dec(
P
)
,
first(
e
)
,
-
n
,
n
+
m
Lemmas
nat
plus
inc
,
Id
wf
,
es-loc
wf
,
es-loc-pred
,
nat
plus
wf
,
nat
plus
properties
,
le
wf
,
decidable
int
equal
,
eqtt
to
assert
,
eqff
to
assert
,
iff
transitivity
,
assert
of
bnot
,
not
functionality
wrt
iff
,
assert
of
eq
int
,
eq
int
wf
,
bool
wf
,
bnot
wf
,
rel
exp
wf
,
not
wf
,
assert
wf
,
first
wf
,
pred
wf
,
es-pred?
wf
,
es-E
wf
,
event
system
wf
origin
es:ES, x, y:E. (x 
x,y. 
first(y) & x = pred(y)^+ y) 
loc(x) = loc(y) 
Id es:ES, x, y:E. (x x,y. first(y) & x = pred(y)^+ y) loc(x) = loc(y) Id T
B(x)
B(x)
bAx.A(x) Qx:A. B(x)
B
x:A. B(x)
b
j
Q
Q